lemmas 0,22
STM: m-sys-at-feasible

STM: m-sys-at wf2

origin